$\forall$${\it es}$:ES, $i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type.
\\[0ex]($\forall$$x$:Id. vartype($i$;$x$) $\subseteq$r ${\it ds}$($x$)?Top) $\Leftarrow\!\Rightarrow$ (state@$i$ $\subseteq$r State(${\it ds}$))